Search for: All records

Worst-case input generation aims to automatically generate inputs that exhibit the worst-case performance of programs. It has several applications, and can, for example, detect vulnerabilities to denial-of-service (DoS) attacks. However, it is non-trivial to generate worst-case inputs for concurrent programs, particularly for resources like memory where the peak cost depends on how processes are scheduled. This article presents the first sound worst-case input generation algorithm for concurrent programs under non-monotone resource metrics like memory. The key insight is to leverage resource-annotated session types and symbolic execution. Session types describe communication protocols on channels in process calculi. Equipped with resource annotations, resource-annotated session types not only encode cost bounds but also indicate how many resources can be reused and transferred between processes. This information is critical for identifying a worst-case execution path during symbolic execution. The algorithm is sound: if it returns any input, it is guaranteed to be a valid worst-case input. The algorithm is also relatively complete: as long as resource-annotated session types are sufficiently expressive and the background theory for SMT solving is decidable, a worst-case input is guaranteed to be returned. A simple case study of a web server's memory usage demonstrates the utility of the worst-case input generation algorithm. 

There are two approaches to automatically deriving symbolic worst-case resource bounds for programs: static analysis of the source code and data-driven analysis of cost measurements obtained by running the program. Static resource analysis is usually sound but incomplete. Data-driven analysis can always return a result, but its lack of robustness often leads to unsound results. This paper presents the design, implementation, and empirical evaluation of hybrid resource bound analyses that tightly integrate static analysis and data-driven analysis. The static analysis part builds on automatic amortized resource analysis (AARA), a state-of-the-art type-based resource analysis method that performs cost bound inference using linear optimization. The data-driven part is rooted in novel Bayesian modeling and inference techniques that improve upon previous data-driven analysis methods by reporting an entire probability distribution over likely resource cost bounds. A key innovation is a new type inference system calledHybrid AARAthat coherently integrates Bayesian inference into conventional AARA, combining the strengths of both approaches. Hybrid AARA is proven to be statistically sound under standard assumptions on the runtime cost data. An experimental evaluation on a challenging set of benchmarks shows that Hybrid AARA (i) effectively mitigates the incompleteness of purely static resource analysis; and (ii) is more accurate and robust than purely data-driven resource analysis. 

Probabilistic programming languages (PPLs) provide language support for expressing flexible probabilistic models and solving Bayesian inference problems. PPLs withprogrammable inferencemake it possible for users to obtain improved results by customizing inference engines usingguideprograms that are tailored to a correspondingmodelprogram. However, errors in guide programs can compromise the statistical soundness of the inference. This article introduces a novel coroutine-based framework for verifying the correctness of user-written guide programs for a broad class of Markov chain Monte Carlo (MCMC) inference algorithms. Our approach rests on a novel type system for describing communication protocols between a model program and a sequence of guides that each update only a subset of random variables. We prove that, by translating guide types to context-free processes with finite norms, it is possible to check structural type equality between models and guides in polynomial time. This connection gives rise to an efficienttype-inference algorithmfor probabilistic programs with flexible constructs such as general recursion and branching. We also contribute acoverage-checking algorithmthat verifies the support of sequentially composed guide programs agrees with that of the model program, which is a key soundness condition for MCMC inference with multiple guides. Evaluations on diverse benchmarks show that our type-inference and coverage-checking algorithms efficiently infer types and detect sound and unsound guides for programs that existing static analyses cannot handle. 

Abstract Melanoma and nonmelanoma skin cancers are among the most prevalent and most lethal forms of skin cancers. To identify new lead compounds with potential anticancer properties for further optimization, in vitro assays combined with in‐silico target fishing and docking have been used to identify and further map out the antiproliferative and potential mode of action of molecules from a small library of compounds previously prepared in our laboratory. From screening these compounds in vitro against A375, SK‐MEL‐28, A431, and SCC‐12 skin cancer cell lines, 35 displayed antiproliferative activities at the micromolar level, with the majority being primarily potent against the A431 and SCC‐12 squamous carcinoma cell lines. The most active compounds11(A431: IC₅₀ = 5.0 μM, SCC‐12: IC₅₀ = 2.9 μM, SKMEL‐28: IC₅₀ = 4.9 μM, A375: IC₅₀ = 6.7 μM) and13(A431: IC₅₀ = 5.0 μM, SCC‐12: IC₅₀ = 3.3 μM, SKMEL‐28: IC₅₀ = 13.8 μM, A375: IC₅₀ = 17.1 μM), significantly and dose‐dependently induced apoptosis of SCC‐12 and SK‐MEL‐28 cells, as evidenced by the suppression of Bcl‐2 and upregulation of Bax, cleaved caspase‐3, caspase‐9, and PARP protein expression levels. Both agents significantly reduced scratch wound healing, colony formation, and expression levels of deregulated cancer molecular targets including RSK/Akt/ERK1/2 and S6K1. In silico target prediction and docking studies using the SwissTargetPrediction web‐based tool suggested that CDK8, CLK4, nuclear receptor ROR, tyrosine protein‐kinase Fyn/LCK, ROCK1/2, and PARP, all of which are dysregulated in skin cancers, might be prospective targets for the two most active compounds. Further validation of these targets by western blot analyses, revealed that ROCK/Fyn and its associated Hedgehog (Hh) pathways were downregulated or modulated by the two lead compounds. In aggregate, these results provide a strong framework for further validation of the observed activities and the development of a more comprehensive structure–activity relationship through the preparation and biological evaluation of analogs. 

Being a fully automated technique for resource analysis, automatic amortized resource analysis (AARA) can fail in returning worst-case cost bounds of programs, fundamentally due to the undecidability of resource analysis. For programmers who are unfamiliar with the technical details of AARA, it is difficult to predict whether a program can be successfully analyzed in AARA. Motivated by this problem, this article identifies classes of programs that can be analyzed in type-based polynomial AARA. Firstly, it is shown that the set of functions that are typable in univariate polynomial AARA coincides with the complexity class PTime. Secondly, the article presents a sufficient condition for typability that axiomatically requires every sub-expression of a given program to be polynomial-time. It is proved that this condition implies typability in multivariate polynomial AARA under some syntactic restrictions.